Nuprl Lemma : gcd_p_functionality_wrt_assoced
2,24
postcript
pdf
a
,
a'
,
b
,
b'
,
y
,
y'
:
. (
a
~
a'
)
(
b
~
b'
)
(
y
~
y'
)
(GCD(
a
;
b
;
y
)
GCD(
a'
;
b'
;
y'
))
latex
Definitions
P
Q
,
a
~
b
,
x
:
A
.
B
(
x
)
,
t
T
,
GCD(
a
;
b
;
y
)
,
x
.
t
(
x
)
,
{
T
}
,
P
Q
,
P
Q
,
Prop
,
b
|
a
,
P
&
Q
Lemmas
divides
wf
,
assoced
weakening
,
divides
functionality
wrt
assoced
,
and
functionality
wrt
iff
,
implies
functionality
wrt
iff
,
all
functionality
wrt
iff
,
iff
functionality
wrt
iff
,
assoced
wf
origin
a, a', b, b', y, y':
. (a ~ a') 
(b ~ b') (y ~ y') (GCD(a;b;y) 
GCD(a';b';y')) a, a', b, b', y, y':. (a ~ a') (b ~ b') (y ~ y') (GCD(a;b;y) GCD(a';b';y')) 
T
x. t(x)